BoolDeq  EqDecider() 

latex

Definitions	EqDecider(T), BoolDeq, <a, b>, x.A(x), bool-deq-aux, p =b q, x:AB(x), P  Q, , , s = t, b, x:A. B(x), f(a), t  T
Lemmas	assert wf, iff wf, bool wf, eq bool wf, bool-deq-aux